\begin{nusmvCommand}{check\_ctlspec} {Performs fair CTL model checking.}

\cmdLine{check\_ctlspec [-h] [-m | -o output-file] [-n number | -p \linebreak"\ctlexpr [IN context]"]}

Performs fair CTL model checking.

A \ctlexpr to be checked can be specified at command line using
option \commandopt{p}. Alternatively, option \commandopt{n} can be
used for checking a particular formula in the property database. If
neither \commandopt{n} nor \commandopt{p} are used, all the SPEC
formulas in the database are checked.\\
\begin{cmdOpt}

\opt{-m}{Pipes the output generated by the command in processing
\code{SPEC}s to the program specified by the \shellvar{PAGER} shell
variable if defined, else through the \unix command
\shellcommand{more}.}

\opt{-o \parameter{\filename{output-file}}}{Writes the output generated by the command in
processing \code{SPEC}s to the file \filename{output-file}.}
            
\opt{-p \parameter{"\ctlexpr [IN context]"}}{A CTL formula to be checked.
\code{context} is the module instance name which the variables in
\ctlexpr must be evaluated in.}

\opt{-n \parameter{\natnum{number}}}{Checks the CTL property with index \natnum{number} in
the property database.} 

\end{cmdOpt}
  If the \envvar{ag\_only\_search} environment variable has been set,
  then a specialized algorithm to check AG formulas is used instead of
  the standard model checking algorithms.

  Since version 2.4.1 this command substitutes \command{check\_spec} that
  is \emph{deprecated}.

\end{nusmvCommand}
